Iof proof for Lemma dcdr-to-bool-equivalence:
1. P :
2. d : Dec(P)
3. P
[d]
by (Unfolds ``decidable`` ( 2)
)
CollapseTHEN (D (-2))
C1:
C1: 2. x : P
C1: 3. P
C1: [inl x ]
C2:
C2: 2. y : 
P
C2: 3. P
C2: [inr y ]
C.| 11,40 |
[d]
by (Unfolds ``decidable`` ( 2))
CollapseTHEN (D (-2))
C1:
C1: 2. x : P
C1: 3. P
C1: [inl x ]
C2:
C2: 2. y : P
C2: 3. P
C2: [inr y ]
C.
| Definitions |  Q |